H. Guo, D. Chen, B. Bentzen; "Verified completeness in Henkin-style for intuitionistic propositional logic"
https://arxiv.org/abs/2310.01916
Memo
Huayu Guo
,
Dongheng Chen
,
Bruno Bentzen
Lean 3
?で
直観主義論理の完全性定理
を証明する
この論文では
直観主義命題論理
に限る.
読んだ上で色々再構成したメモ書きが↓にある
直観主義命題論理のプライム性を用いたKripke完全性定理